a,b:. divides(a; b)  divides(b; a)  pm_equal(a; b) 

latex

Definitions	t  T, P  Q, x:A. B(x), P  Q, P  Q, P  Q, x. t(x), prop{i:l}, x(s),
Lemmas	divides wf, divides of absvals, absval eq, divides anti sym n, absval elim, all functionality wrt iff, iff transitivity, absval wf, nat wf